M1, M2:MsgA. M1 = M2  M1  M2 

latex

Definitions	t  T, x:A. B(x), M1  M2, MsgA, Prop, P  Q, IdLnk, Id, product-deq(A;B;a;b), Knd, IdLnkDeq, x. t(x), 2of(t), rcv(l,tg), f(x)?z, Top, 1of(t), State(ds), locl(a), KindDeq, IdDeq, f  g, P & Q, A & B, Valtype(da;k)
Lemmas	fpf-sub weakening, Id wf, id-deq wf, Knd wf, Kind-deq wf, locl wf, IdLnk wf, ma-state wf, pi1 wf, top wf, fpf-cap wf, rcv wf, pi2 wf, idlnk-deq wf, product-deq wf, msga wf, ma-sub wf